R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
R2(P(P(x1))) → P2(P(r(x1)))
R2(p(x1)) → P2(x1)
R2(P(P(x1))) → P2(r(x1))
R2(p(x1)) → P1(r(P(x1)))
R2(P(P(x1))) → R2(x1)
R2(p(x1)) → R2(P(x1))
R2(p(x1)) → P1(p(r(P(x1))))
R1(x1) → R2(x1)
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
R2(P(P(x1))) → P2(P(r(x1)))
R2(p(x1)) → P2(x1)
R2(P(P(x1))) → P2(r(x1))
R2(p(x1)) → P1(r(P(x1)))
R2(P(P(x1))) → R2(x1)
R2(p(x1)) → R2(P(x1))
R2(p(x1)) → P1(p(r(P(x1))))
R1(x1) → R2(x1)
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
R2(P(P(x1))) → R2(x1)
R2(p(x1)) → R2(P(x1))
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R2(p(x1)) → R2(P(x1))
Used ordering: Polynomial interpretation [25,35]:
R2(P(P(x1))) → R2(x1)
The value of delta used in the strict ordering is 9.
POL(P(x1)) = (4)x_1
POL(R2(x1)) = (4)x_1
POL(p(x1)) = 9/4 + (4)x_1
P(p(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
R2(P(P(x1))) → R2(x1)
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R2(P(P(x1))) → R2(x1)
The value of delta used in the strict ordering is 1/4.
POL(P(x1)) = 1/4 + x_1
POL(R2(x1)) = (1/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
R(x1) → r(x1)
r(p(x1)) → p(p(r(P(x1))))
r(r(x1)) → x1
r(P(P(x1))) → P(P(r(x1)))
p(P(x1)) → x1
P(p(x1)) → x1
r(R(x1)) → x1
R(r(x1)) → x1